es:ES, ff:FIFO, is_req, is_ack:(E), awaiting, owes_ack:(IdIdId).
(ff.C r Id)
 (i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 (e:E. Dec(is_req(e)) & Dec(is_ack(e)))
 (i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
 (sndr, rcvr:ff.C, e:E.
 [e: rcvr is_ack sndr]  (x:E. ((x < e) & [x: sndr is_req rcvr]))) 

latex

Definitions

x:A. B(x), (e < e'), [e: i p j], plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack), ff.S, Dec(P), P  Q, ff.R, s = t, loc(e), P & Q, x:A  B(x), @i(x:T), , f(a), ff.C, Id, x:AB(x), E, , Type, FIFO, x:A. B(x), t  T, ES, (e <loc e'), [e: i p j], ff.Sender, for clients C sends FIFO   from j to i via (S[j,i],codes)   receives at i via (R[i],decodes), state@i, {x:A| B(x)} , let x,y = A in B(x;y), e < e', A c B, t.1, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), A, b, True

Lemmas

es-causle weakening, es-causl transitivity2, fifoSender-causes, es-causl weakening, snd-it-of-rcv-it, es-causl wf, fifoSender wf, req-received-before-ack, event system wf, FIFO wf, es-E wf, Id wf, fifoC wf, es-dtype wf, bool wf, es-loc wf, fifoR wf, decidable wf, fifoS wf, plus-ify wf, snd-it wf